import java.awt.Point;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;

/**
 * Class that describe the Solver process of our solution.
 * Provide to create the clause provided in it's sat variable.
 * Then executes the miniwrapper solver that,using minisat,provide to determine
 * if the problem formulated with the following clause is satisfiable of not.
 * Whenever it's satisfiable we print out the respective variable that solve the equations. 
 * 
 * @author Scinetti,Trombini,Garcia Fernandez
 *
 */

public class Solver {

	
	private Graph graph;
	private String codeRule;
	public static final String AND = "$\n";
	public static final String OR = " ";
	public static final String NOT = "~";

	public Solver(final ArrayList<String> satVariable) {
       this.codeRule = "";
	}

	public Solver(final Graph graph){
		this.graph = graph;
		this.codeRule = "";
	}
	
	/**
	 * method that defines the rules to pass
	 * on the sat solver minisat
	 */

	public void defineRule() {
//		int size = this.satVariable.size();
//
//		for (int i = 0; i < size; i++) {
//
//			// we start to compose our rule
//			String variable = satVariable.get(i);
//			
//			String startsWith = variable.split("y")[0].substring(1);
//			String endsWith = variable.split("y")[1];
//
//			// add rule that affirm that an edge can not contain it's reverse
//
//			codeRule += NOT + variable + OR + NOT
//					+ reverseEdge(startsWith, endsWith) + AND;
//
//			// add rule that affirm that and edge
//
//			for (int j = 0; j < size; j++) {
//				String subVariable = satVariable.get(j);
//
//				if (subVariable != variable) {
//					// System.out.println(variable.split("y")[0]+"::"+subVariable.split("y")[0]);
//					if (variable.split("y")[0]
//							.equals(subVariable.split("y")[0])) {
//						codeRule += NOT + variable + OR + NOT + subVariable
//								+ AND;
//					}
//					if (("y" + variable.split("y")[1]).equals("y"
//							+ subVariable.split("y")[1])) {
//						codeRule += NOT + variable + OR + NOT + subVariable
//								+ AND;
//					}
//
//				}
//			}
//
//			codeRule += variable;
//			for (int k = 0; k < size; k++) {
//				String subVariable = satVariable.get(k);
//				if (subVariable != variable) {
//					if (variable.split("y")[0]
//							.equals(subVariable.split("y")[0])) {
//						codeRule += OR + subVariable;
//					}
//				}
//			}
//			codeRule += AND;
		 
		
//		} // end restriction rule
	}

	
    public void defineRuleNew(){
    	codeRule = "";
    	int size = graph.V.size(); 
    	
    	//total clause : Every vertex in V maps to at least one position in H
    	for(int i=1;i <= size;i++){
    		for(int j=1;j <= size ;j++){
    			codeRule += "v"+i+"p"+j+" ";
    		}
    	 codeRule += AND;
    	
    	
    	//functional clause : Every vertex maps to at most one position
    	for(int j=1;j <= size;j++){
    	 	for(int k=j+1;k <= size;k++){
    			codeRule += NOT+"v"+i+"p"+j+OR+NOT+"v"+i+"p"+k+" "+AND;
    		}
    	
    	 }
    	}
    	
    	//ONTO: Every position in H has at least one vertex mapped to it.
    	for(int j=1;j <= size;j++){
    		for(int i=1;i <= size ;i++){
    			codeRule += "v"+i+"p"+j+" ";
    		}
    	 codeRule += AND;
    	
    	
    	//1 to 1: At most one vertex maps to each position.
    	for(int i=1;i <= size;i++){
    		for(int k=i+1;k <= size;k++){
    			codeRule += NOT+"v"+i+"p"+j+" "+NOT+"v"+k+"p"+j+" "+AND;
    		}
    
    	 }
    	}
    	
    	//edge rule
    	for(int i=1;i <= size;i++){
    		for(int j=1;j <= size;j++){
    			
    				
    					Point p1 = new Point(graph.V.get(i-1),graph.V.get(j-1));
    					Point p2 = new Point(graph.V.get(j-1),graph.V.get(i-1));
    			     if(!graph.E.contains(p1) && !graph.E.contains(p2)){
    			    	 for(int k=1;k <= size;k++){
    			    	 codeRule += NOT+"v"+i +"p"+k + OR +
 						NOT+"v"+j+"p"+((k+1) % size) +" "+AND;
    			    	 codeRule += NOT+"v"+i +"p"+((k+1) % size) 
    			    	 + OR +NOT+"v"+j+"p"+k +" "+AND;
    			     
    			   }
    			}
    		}
    	  }
    	
    }
	
	/**
	 * method that execute the miniwrapper command given a 
	 * set of rules:
	 * 
	 * Executes the miniwrapper command as follows
	 * ./miniwrapper -m [filename_input] > [filename_output]
	 * @throws IOException
	 */

	public void execute() throws IOException {

		// create the file named "input.txt" that contain the set of rules

		File file = new File(Main.PATH + Main.FILE_INPUT);
		file.createNewFile();
		FileWriter fstream = new FileWriter(Main.PATH + Main.FILE_INPUT);
		BufferedWriter out = new BufferedWriter(fstream);
		out.write(getCodeRule());
		out.close();

		// execute the miniwrapper command,then write the result on
		// "output.txt" file
        String command = "sh job.sh ../"+Main.FILE_INPUT + " ../" +Main.FILE_OUTPUT;
		Process p = Runtime.getRuntime().exec(command);

		BufferedReader input = new BufferedReader(new InputStreamReader(
				p.getErrorStream()));
		String line;
		while ((line = input.readLine()) != null) {
			System.out.println(line);
		}

		input.close();
		p.destroy();

	}

	/**
	 * Method that return the all the variables 
	 * and clauses used to store the information
	 * 
	 * @return
	 */

	public String getCodeRule() {
		return codeRule;
	}

}
